Nuprl Definition : product-deq
11,40
postcript
pdf
product-deq(
A
;
B
;
a
;
b
) == <proddeq(
a
;
b
),
p
,
q
. <
x
.axiom,
x
.axiom>>
latex
Definitions
proddeq(
a
;
b
)
,
<
a
,
b
>
,
x
.
A
(
x
)
,
axiom
FDL editor aliases
product-deq
origin
p,q. <x.axiom, x.axiom>> p,q. <x.axiom, x.axiom>> x.A(x)